COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.if false then begin "notes"
C00003 00003	.begin "bib mode"
C00012 ENDMK
C⊗;
.if false then begin "notes"

add sussman and steele references  (most can be found in FACT.F78[206,LSP])


LSPBIB[LSP,CLT] BIBLIOGRAPHY
   more annotation
   more references merge class biblist etc.
   selectivley-exhaustive lit survey???

ref to Wegbreit w respect to derived programs


.end "notes"
.begin "bib mode"
.s(BIBLIO,BIBLIOGRAPHY)
.indent 0,4
.skip 3

%3Allen, John R. [1979]%*:  ⊗⊗The Anatomy of LISP⊗, McGraw-Hill.

%3Baker, Henry G. [1978]%*:  "List Processing in Real TIme on a Serial Computer",
⊗⊗Communications of the ACM⊗ %321%*, pp. 280-294.

	Description and analysis of a list processing system that continuously 
reclaims garbage while linearizing and compacting space in use.

%3Boyer, Robert S. and J. Strother Moore [1978]%*:
⊗⊗A Computational Logic⊗, Academic Press, New York, xiv + 397 pp.

%3Brudno, A. L. [1963]%*:  
"Bounds and Valuations for Shortening the Scanning of Variations",
[in Russian], ⊗⊗Problemy Kibernetiki⊗ %310%* pp.141-150.

	First published account of the ααβ algorithm.

%3Cartwright, Robert [1977]%*:  
%2Practical Formal Semantic Defintion and Verification Systems,%1
Ph.D. thesis, Computer Science Department, Stanford University, Stanford, Ca..

%3Davis, Martin [1958]%*:
%2Computability and Unsolvability%1, McGraw-Hill.

This book contains many unsolvability theorems.

%3Filman, R. E. and R. W. Weyhrauch [1976]%*: ⊗⊗A FOL Primer⊗, Stanford Artificial
Intelligence Laboratory Memo AIM-288.

	An excellent introduction to using the automatic first order logic
proof checker FOL.  

%3Gordon, M. [1975]%*:  %2Operational Reasoning and Denotational Semantics%1,
Stanford Artificial Intelligence Laboratory Memo, AIM-264.

%3Kleene, Stephen C. [1952]%*: %2Introduction to Metamathematics%1,
Van Nostrand.

This is the standard work on recursive function theory.

%3Knuth, D. E. [1968a]%*:  ⊗⊗The Art of Computer Programming, Vol. I:
Fundamental Algorithms⊗.  Addison-Wesley.

	Section qsect2.3.5 contains a discussion of list structures and 
garbage collection algorithms.

%3Knuth, D. E. [1968b]%*:  ⊗⊗The Art of Computer Programming, Vol. III:
Sorting and Searching⊗.  Addison-Wesley.

	Section qsect6.4 contains a discussion of hashing.

%3Knuth, D. E. and R. Moore [1975]%*:  "An Analysis of Alpha-Beta Pruning",
⊗⊗Artificial Intelligence⊗, %36%*.

	A history, description, and analysis of the ααβ algorithm.

%3Manna, Zohar [1974]%*: ⊗⊗Mathematical Theory of Computation⊗, McGraw-Hill.

	Chapter 2 contains a discussion of first order logic and of the
⊗natural_deduction method of proof.

	Chapter 5 contains a discussion of functionals and fixedpoints.  

	The book also contains
a discussion of structural induction and other methods of proving properties
of programs.  

%3McCarthy, John [1962a]%*: "Computer Programs for Checking Mathematical
Proofs", in ⊗⊗Proc. Symp. Pure Math.⊗ Vol.5 , Amer. Amth. Soc.,
Providence, R. I., pp219-227.

%3McCarthy, John [1962b]%*:  "Towards a Mathematical Science of Computation,"
in C. M. Popplewell (ed.), ⊗⊗Information Processing, Proceedings of IFIP
Congress 62⊗, pp21-28, North Holland Publishing Company, Amsterdam.

	Contains discussions of transforming Flow Chart programs into
recursive programs and of the Abstract Syntax of programming languages.

%3McCarthy, John [1963]%*: "A Basis for a Mathematical Theory of Computation",
in P. Braffort and D. Hirschberg (eds.), ⊗⊗Computer Programming and Formal
Systems⊗, pp. 33-70. North-Holland Publishing Company, Amsterdam.

	Contains a complete discussion of properties of conditional forms,
including canonical forms.  Also discusses computable functionals and
recursion induction.

%3McCarthy, John [1964]%*:  "A Formal Description of a Subset of Algol",
⊗⊗Proc. Conf. on Formal Language Description Languages⊗, Vienna.


%3McCarthy, John [1978a]%*:  
"History of LISP", in
⊗⊗Proceedings of the ACM conference on History of Programming Languages⊗, 1978.

%3McCarthy, John [1978b]%*:  "Representation of Recursive Programs in
First Order Logic", in ⊗⊗Proceedings the International Conference on
Mathematical Studies of Information Processing⊗, Kyoto Japan, 1978.

%3McCarthy, John and James Painter [1967]%*: "Correctness of a Compiler 
for Arithmetic Expressions", ⊗⊗Proceeding of Symposia in Applied 
Mathematics⊗, Vol. 19, J. T. Schwartz (ed.),
American Mathematical Society, pp 33-41.

%3Moszkowski, B. [1978]%*: informal memo

%3Nilsson, N. J. [1971]%*:  ⊗⊗Problem Solving Methods in Artificial Intelligence⊗,
McGraw-Hill.

%3Painter, James [1967]%*:  %2Semantic Correctness of a Compiler for an
Algol-like Language%1, Ph.D. thesis, Computer Science Department, 
Stanford University, Stanford, Ca..

%3Steele, G.L. [1978]%*: %2RABBIT: A Compiler for SCHEME%1 M.S.
thesis, Department of Electrical Engineering and Computer Science, M.I.T.%*

%3Sussman, G.J. and G.L. Steele[1978]:%* 
%2The revised report on SCHEME, a Dialect of LISP%2, MIT-AI Memo 452.

%3Vuillemin, J. [1973]%*: %2Proof Techniques for Recursive Programs,%1 Ph.D.
thesis, Computer Science Department, Stanford University, Stanford, Ca..

%3Weyhrauch, R. W. [1977]%*:  %2A users manual for FOL%1, Stanford Artificial
Intelligence Laboratory Memo, AIM-235.1.

	A manual for the automatic proof checker FOL.

%3Winston, P. H. [1977]%*:  ⊗⊗Artificial Intelligence⊗,  Addison-Wesley.

.end "bib mode"